| Definitions | P   Q,  x:A. B(x), Id, f(x), t.2, Knd, t  T, Top, a:A fp B(a), kind(e), x dom(f),  b, state@i, ma-interface-ds(I;i), State(ds), valtype(e), t.1, P & Q, s = t, E, Type, left + right, x:A B(x), x:A  B(x), [[I|i]], ma-interface-consistent(es;X), e  X, loc(e), <a, b>, (x l), ma-interface-consistent2(es;I), MaInterface(T), ES, {x:A| B(x)} ,   x. t(x), type List, Atom$n, e@i. P(e), a < b, if b then t else f fi , P  Q, P Q, IdDeq, x.A(x), hasloc(k;i),  x:A. B(x), let x,y = A in B(x;y), case b of inl(x) => s(x) | inr(y) => t(y), S  T,  , IdLnk, KindDeq, Void,  x:A.B(x), fpf-domain(f), Dec(P), f(a), {T}, SQType(T), s ~ t, ma-interface-dom(I;i), ma-interface-info(I;i;k), ma-interface-valtype(I;i;k), f(x)?z, vartype(i;x),  |